/*
 * Ta klasa ma za zadanie rozwiązać pojedynczą formułę, tj. wskazać podstawienie
 * lub powiedzieć, że nie ma takiego
 */
package sat;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.Iterator;
import java.util.Vector;
import sat.convenience.Population;
import sat.convenience.Solution;
import sat.exceptions.ParseException;

import java.io.InputStreamReader;

import java.lang.management.ManagementFactory;

public class Solver {

    private static Solver instance;
    private Vector<FormulaCNF> formulae;
    private Vector<Vector<Solution>> solutions;
    private Vector<Vector<Float>> times;
    private Vector<Solution> emptySolutions = new Vector<Solution>();
    public boolean verbose = false;

    public static void main(String[] args) {
        {
            String filename = "formulae";
            boolean proceed = false;
            boolean algoritm = false;
            int epochs = 1;

            Solver solver = Solver.getInstance();

            for (int i = 0; i < args.length; ++i) {
                if (args[i].equals("-f") && args.length > i) {
                    filename = args[++i];
                } else if (args[i].equals("-v")) {
                    solver.verbose = true;
                    System.out.println("verbose mode enabled");
                }
            }

            try {
                solver.decorate(null);solver.decorate("SAT problem");solver.decorate(null);
                solver.loadFile(filename);

                solver.mapVariables();
                solver.printRaw();

                InputStreamReader inputStreamReader = new InputStreamReader(System.in);
                BufferedReader reader = new BufferedReader(inputStreamReader);

                while (proceed != true) {
                    try {
                        System.out.println("Please specify the number of repetitions: ");
                        epochs = Integer.parseInt(reader.readLine());
                        proceed = true;
                    } catch (Exception e) {
                    }
                }


                while(algoritm != true)
                {
                    solver.decorate(null);
                    System.out.println("press g - to run gsat algoritm");
                    System.out.println("press s - to run sasat algoritm");
                    System.out.println("press e - to run evosat algoritm");
                    solver.decorate(null);
                    System.out.println("or q to quit");
                    solver.decorate(null);
                    System.out.println("or a: auto");
                    solver.decorate(null);

                    String str = reader.readLine();


                    if (str.charAt(0) == 'q') {
                        System.out.println("bye!");
                        return;
                    }

                    if (str.charAt(0) == 'g') {
                        int maxtries = 0, maxflips = 0;

                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("maxtries: ");
                                maxtries = Integer.parseInt(reader.readLine());
                                if (maxtries > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("maxflips: ");
                                maxflips = Integer.parseInt(reader.readLine());
                                if (maxflips > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }

                        for (int i = 0; i < epochs; ++i) {
                            solver.gsatBatch(maxtries, maxflips, 1, false);
                        }
                        solver.printAll();
                       //algoritm = true; //jezeli nie ma tej linijki to program sie zapetla
                    } else if (str.charAt(0) == 's') {
                        int maxtries = 0;
                        float decayRate = 0f, tMax = 0f, tMin = 0f;

                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("enter the number of max tries (i): ");
                                maxtries = Integer.parseInt(reader.readLine());
                                if (maxtries > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("define the decay rate (f): ");
                                decayRate = Float.parseFloat(reader.readLine());
                                if (decayRate > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("define max temperature (f): ");
                                tMax = Float.parseFloat(reader.readLine());
                                if (tMax >= 1)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("define min temperature (f): ");
                                tMin = Float.parseFloat(reader.readLine());
                                if (tMin >= 0 && tMin <= tMax)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }

                        for (int i = 0; i < epochs; ++i) {
                            solver.sasatBatch(maxtries, decayRate, tMax, tMin, false);//(1, 2f, 30f, 0f, true);
                        }
                        solver.printAll();
                        //algoritm = true; //jezeli nie ma tej linijki to program sie zapetla
                    } else if (str.charAt(0) == 'e') {
                        int maxGenerations = 0, populationSize = 0;
                        float localSearchThreshold = 0f;

                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("maxGenerations: ");
                                maxGenerations = Integer.parseInt(reader.readLine());
                                if (maxGenerations > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("populationSize: ");
                                populationSize = Integer.parseInt(reader.readLine());
                                if (populationSize > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }
                        proceed = false;
                        while (proceed != true) {
                            try {
                                System.out.println("localSearchThreshold: ");
                                localSearchThreshold = Float.parseFloat(reader.readLine());
                                if (localSearchThreshold > 0)
                                    proceed = true;
                            } catch (Exception e) {
                            }
                        }

                        for (int i = 0; i < epochs; ++i) {
                            solver.evosatBatch(maxGenerations, populationSize, localSearchThreshold, 1.0f, false, 1);//140, 1, 0.4f
                        }
                        solver.printAll();
                        //algoritm = true; //jezeli nie ma tej linijki to program sie zapetla
                    } else if (str.charAt(0) == 'a') {

                        for (int i = 0; i < epochs; ++i) {
                            //solver.gsatBatch(5, 50, 1, false);
                            //solver.evosatBatch(140, 10, 0.4f, 1.0f, false, 1);
                            solver.sasatBatch(1, 2f, 30f, 0f, false);
                            long stop_time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId());
                        }
                        solver.printAll();
                        //algoritm = true; //jezeli nie ma tej linijki to program sie zapetla
                    }
                }

            } catch (Exception e) {
                System.err.println(e.toString());
                e.printStackTrace();
            }
        }
    }

    public void startEpoch() {
        this.solutions.add(new Vector<Solution>());
        this.times.add(new Vector<Float>());
    }

    //returns an instane of solver
    public static Solver getInstance() {
        if (instance == null) {
            instance = new Solver();
        }
        return instance;
    }

    private Solver() {
        formulae = new Vector<FormulaCNF>();
        solutions = new Vector<Vector<Solution>>();
        times = new Vector<Vector<Float>>();
    }

    public void mapVariables() {
        for (int i = 0; i < formulae.size(); ++i) {
            emptySolutions.add(formulae.get(i).getUniqueLiterals());
        }
    }

    public void loadFile(String path) throws IOException, ParseException {
        File f = new File(path);
        BufferedReader br = new BufferedReader(new FileReader(f));
        String line;
        while ((line = br.readLine()) != null) {
            if (line.length() > 0) {
                formulae.add(new FormulaCNF(line));
            }
        }
        br.close();
    }

    public void decorate(String text){
        System.out.println("= = = = = "+(text!=null?text:"= = = = = = = =")+" = = = = = ");
    }
    
    public void printRaw() {
        decorate("Loaded problems:");
        for (int i = 0; i < formulae.size(); ++i) {
            System.out.println("P" + i + ": " + formulae.get(i));
        }
    }

    public void printAll() {
        decorate("Obtained solutions:");
        for (Vector<Solution> s : solutions) {
            for (Solution solution : s) {
                System.out.println(solution);
            }
        }
        decorate("Execution statistics:");
        for (int i = 0; i < formulae.size(); ++i) {
            Vector<Float> mam = getMinAvgMaxCorrect(i);
            System.out.println("P" + i + "(" + mam.get(3) + "%):  t min: " + mam.get(0) + "ms, t avg: " + mam.get(1) + "ms, t max: " + mam.get(2) + "ms");
        }
    }

    /**
     * GSAT batch function, attempts to solve all the Solver.formulae
     * @param maxtries - self-explanatory
     * @param maxflips - self-explanatory
     * @param distance - neighborhood radius, currently supports only 1
     * @param noRandomStart - if true, the algorithm will attempt to find a solution 
     * by means of exploring the neighborhood of current solution (Solver.solutions[i])
     */
    private void gsatBatch(int maxtries, int maxflips, int distance, boolean noRandomStart) {
        startEpoch();
        for (int i = 0; i < formulae.size(); ++i) {
            if (verbose) {
                System.out.println("Gsat epoch: " + times.size() + " Problem: " + i);
            }
            long time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId());
            Solution solution = gsat(formulae.get(i), maxtries, maxflips, distance,
                    noRandomStart ? formulae.get(i).getUniqueLiterals() : null);
            time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId()) - time;
            float executionTime = (solution != null ? time / 10e6f : Float.NEGATIVE_INFINITY);
            if (verbose) {
                System.out.println("Final solution: " + solution);
            }
            times.get(times.size() - 1).add(executionTime);
            solutions.get(solutions.size() - 1).add(solution);
            try {
                Thread.sleep(20);
            } catch (Exception e) {
            }
        }
    }

    /**
     * Simulated annealing batch function, attempts to solve all the Solver.formulae
     * @param maxtries  - self-explanatory
     * @param decayRate - self-explanatory
     * @param tMax      - self-explanatory
     * @param tMin      - self-explanatory
     * @param noRandom  - if true, the algorithm will attempt to find a solution 
     * by means of exploring the neighborhood of current solution (Solver.solutions[i])
     */
    private void sasatBatch(int maxtries, float decayRate, float tMax, float tMin, boolean noRandom) {
        startEpoch();
        for (int i = 0; i < formulae.size(); ++i) {
            if (verbose) {
                System.out.println("Sasat epoch: " + times.size() + " Problem: " + i);
            }
            long time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId());
            Solution solution = sasat(formulae.get(i), maxtries, decayRate, tMax, tMin,
                    noRandom ? formulae.get(i).getUniqueLiterals() : null);
            time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId()) - time;
            float executionTime = (solution != null ? time / 10e6f : Float.NEGATIVE_INFINITY);
            times.get(times.size() - 1).add(executionTime);
            solutions.get(solutions.size() - 1).add(solution);
            if (verbose) {
                System.out.println("Final solution: " + solution);
            }
            try {
                Thread.sleep(20);
            } catch (Exception e) {
            }
        }
    }

    /**
     * Evolutionary approach, attempts to solve all the Solver.formulae.
     * Used in conjunction with a local search method in attempt to speed up
     * the progress once a maximum seems close enough.
     * @param maxGenerations - number of cross-breeding iterations
     * @param populationSize - self-explanatory
     * @param mutationProbability
     * @param localSearchThreshold - minimum quality required to start a local search
     * @param offspringOnly - if true, the parent individuals are discarded at each breeding
     * @param intermediateToParentsRatio - ratio of intermediate offspring individuals number to parents number 
     * iterations and only the offspring can form the successive generation
     * 
     */
    private void evosatBatch(int maxGenerations,
            int populationSize,
            float mutationProbability,
            float localSearchThreshold,
            boolean offspringOnly,
            int intermediateToParentsRatio) {
        startEpoch();
        for (int i = 0; i < formulae.size(); ++i) {

            if (verbose) {
                System.out.println("Evosat epoch: " + times.size() + " Problem: " + i);
            }
            long time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId());
            Solution solution = evosat(formulae.get(i), maxGenerations, populationSize,
                    localSearchThreshold, offspringOnly, mutationProbability,
                    intermediateToParentsRatio);
            time = ManagementFactory.getThreadMXBean().getThreadCpuTime(Thread.currentThread().getId()) - time;
            float executionTime = (solution != null ? time / 10e6f : Float.NEGATIVE_INFINITY);
            times.get(times.size() - 1).add(executionTime);
            solutions.get(solutions.size() - 1).add(solution);
            if (verbose) {
                System.out.println("Final solution: " + solution);
            }
            try {
                Thread.sleep(20);
            } catch (Exception e) {
            }
        }
    }

    /**
     * Single formula solving function using GSAT algorithm.
     * @param problem - formula being solved 
     * @param maxtries 
     * @param maxflips
     * @param distance 
     * @param initial - initial solution; if provided, the exploration of neighborhood will set off from here
     * @return A - solution if found, null otherwise
     */
    private Solution gsat(FormulaCNF problem, int maxtries, int maxflips, int distance, Solution initial) {
        for (int attempt = 0; attempt < maxtries; ++attempt) {
            Solution candidate = (initial == null ? GsatToolkit.randomize(problem.getUniqueLiterals()) : (Solution) initial.clone());
            for (int flip = 0; flip < maxflips; ++flip) {
                if (problem.evaluate(candidate)) {
                    return candidate;
                }
                Vector<Solution> area = GsatToolkit.getNeighborhood(candidate, distance);
                Solution copy = (Solution) candidate.clone();
                candidate = GsatToolkit.getBest(problem, candidate, area);
                if (verbose) {
                    System.out.println("attempt: " + (attempt + 1) + " flips made: " + (flip + 1));
                    System.out.println((candidate != null ? candidate+
                            " fitness: "+problem.getTrueClausesPercentage(candidate)+ ", weighed: "+problem.getWeighedTrueClausesPercentage(candidate) 
                            : "dead end: " + copy)
                            );
                }
                if (candidate == null) {
                    //dead-end met
                    break;
                }
            }
        }
        return null;
    }

    /**
     * Single formula solving function using simulated annealing algorithm.
     * @param maxtries
     * @param decayRate
     * @param tMax
     * @param tMin
     * @param initial - initial solution; if provided, the exploration of neighborhood will set off from here
     * @return A solution if found, null otherwise.
     */
    private Solution sasat(FormulaCNF problem, int maxtries, float decayRate, float tMax, float tMin, Solution initial) {
        for (int attempt = 0; attempt < maxtries; ++attempt) {

            Solution candidate = initial == null ? GsatToolkit.randomize(problem.getUniqueLiterals()) : (Solution) initial.clone();

            float t = tMax;
            for (int iteration = 0; t > tMin; t = tMax * (float) Math.pow(Math.E, -1 * (iteration++) * decayRate)) {
                //System.out.println("attempt: "+attempt+". iteration: "+iteration);
                if (problem.evaluate(candidate)) {
                    return candidate;
                }
                if (verbose) {
                    System.out.println("attempt: " + (attempt + 1) + " temperature: " + (t));
                    System.out.println(candidate);
                }
                for (Iterator it = candidate.keySet().iterator(); it.hasNext();) {
                    String key = (String) it.next();
                    float potentialGain = SasatToolkit.calculatePotentialGain(problem, candidate, key);
                    float probability = (float) Math.pow(1 + (float) Math.pow(Math.E, -1 * potentialGain / t), -1);
                    if ((float) Math.random() <= probability || potentialGain>0) {
                        candidate.put(key, candidate.get(key).booleanValue() ? Boolean.FALSE : Boolean.TRUE);
                        break;
                    }
                }
            }
        }
        return null;
    }

    /**
     * Single formula solving function using evolutionary approach.
     * Summary:
     * 1. Parents for cross-breading are selected in accordance to Monte Carlo rule.
     * 2. Products of breeding constitute the intermediate offspring
     * 3. Optionally, parents might be introduced into the intermediate offspring.
     * 4. Intermediate offspring is subject to mutation. Modified individuals are added, not replaced.
     * 5. Best individuals form the next generation (quite an exploitive approach)
     * @param problem - formula being solved
     * @param problem
     * @param maxGenerations
     * @param populationSize
     * @param localSearchThreshold - fitness level of individual(0-1),
     * that once crossed triggers a local search with sasat.
     * @param offspringOnly
     * @param mutationProbability - the probability of each offspring individual's bit to be flipped during the mutation phase
     * @param intermediateToParentsRatio - determines the size of intermediate offspring in relation to its parent generation 
     * @return A solution if found, null otherwise.
     */
    private Solution evosat(FormulaCNF problem, int maxGenerations, int populationSize,
            float localSearchThreshold, boolean offspringOnly, float mutationProbability,
            int intermediateToParentsRatio) {
        Population lambda;
        Population mi = null;
        lambda = EvosatToolkit.generatePopulation(populationSize, problem.getUniqueLiterals());

        for (int generation = 0; generation < maxGenerations; ++generation) {
            mi = new Population();
            //check for a winner
            Solution candidate = EvosatToolkit.evaluatePopulation(problem, lambda);
            if (candidate != null) {
                return candidate;
            }
            float minFitness = Float.POSITIVE_INFINITY;
            float maxFitness = Float.NEGATIVE_INFINITY;
            float avgFitness = 0;
            for (Solution s : lambda) {
                float fitness = problem.getWeighedTrueClausesPercentage(s);
                minFitness = Math.min(fitness, minFitness);
                maxFitness = Math.max(fitness, maxFitness);
                avgFitness += fitness;
                if (fitness > localSearchThreshold) {
                    //here a local, sasat search is launched
                    Solution localResult = sasat(problem, 1, 0.1f, 100f, 0.01f, s);
                    if (localResult != null) {
                        return localResult;
                    }
                }
            }
            avgFitness /= lambda.size();
            if (verbose) {
                System.out.println("generation: " + generation + ", min fitness: " + minFitness + ", avg fitness: " + avgFitness + ", max fitness: " + maxFitness);
            }
            mi = EvosatToolkit.generateOffspring(problem, lambda, intermediateToParentsRatio);
            if (!offspringOnly) {
                mi.addAll(lambda);
            }

            lambda = EvosatToolkit.applyMutations(mi, mutationProbability);

            lambda = EvosatToolkit.performSelection(problem, lambda, offspringOnly, populationSize);
        }
        return null;
    }

    private Vector<Float> getMinAvgMaxCorrect(int problem_index) {
        float sum = 0;
        float min = Float.POSITIVE_INFINITY;
        float max = Float.NEGATIVE_INFINITY;
        int failures = 0;
        for (Vector<Float> vt : times) {
            float time = vt.get(problem_index);
            if (time < 0f) {
                failures++;
                continue;
            }

            max = Math.max(max, time);
            min = Math.min(min, time);
            sum += time;
        }
        Vector<Float> result = new Vector<Float>();
        result.add(min);
        result.add(sum / times.size());
        result.add(max);
        result.add((times.size() - failures) * 100f / (float) times.size());
        return result;
    }
}
